Nuprl Definition : p-open 11,40

p-open(p)
== {C:(n:  ({0..n}Outcome)){0..2}| 
== {s:(Outcome), j:i:{0..j}. (C(<is>))  (C(<js>))}  
latex



clarification:

p-open(p)
== {C:(n:  ({0..n}p-outcome(p))){0..2}| 
== {s:(p-outcome(p)), j:i:{0..j}. (C(<is>))  (C(<js>))}  
latex


Definitions{x:AB(x)} , x:A  B(x), x:AB(x), Outcome, , x:AB(x), {i..j}, #$n, A  B, f(a), <ab>
FDL editor aliasesp-open

origin